a,b:. coprime(a; b)  (x,y:. (((a * x) + (b * y)) = 1)) 

latex

Definitions	t  T, P  Q, x:A. B(x), prop{i:l}, x:A. B(x), P  Q, P  Q, P  Q
Lemmas	coprime wf, coprime bezout id0, assoced elim, minus functionality wrt eq